'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ q0(a(x1)) -> x(q1(x1))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q2(x(x1)) -> x(q0(x1))
, q0(y(x1)) -> y(q3(x1))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ q0^#(a(x1)) -> c_0(q1^#(x1))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q3^#(bl(x1)) -> c_12()}
The usable rules are:
{ q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
The estimated dependency graph contains the following edges:
{q0^#(a(x1)) -> c_0(q1^#(x1))}
==> {q1^#(y(x1)) -> c_2(y^#(q1(x1)))}
{q0^#(a(x1)) -> c_0(q1^#(x1))}
==> {q1^#(a(x1)) -> c_1(a^#(q1(x1)))}
{q1^#(a(x1)) -> c_1(a^#(q1(x1)))}
==> {a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))}
{q1^#(a(x1)) -> c_1(a^#(q1(x1)))}
==> {a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))}
{q1^#(a(x1)) -> c_1(a^#(q1(x1)))}
==> {a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))}
{q1^#(y(x1)) -> c_2(y^#(q1(x1)))}
==> {y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))}
{q1^#(y(x1)) -> c_2(y^#(q1(x1)))}
==> {y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))}
{q1^#(y(x1)) -> c_2(y^#(q1(x1)))}
==> {y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))}
{a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))}
==> {q2^#(x(x1)) -> c_9(q0^#(x1))}
{a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))}
==> {q2^#(x(x1)) -> c_9(q0^#(x1))}
{a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))}
==> {q2^#(x(x1)) -> c_9(q0^#(x1))}
{y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))}
==> {q2^#(x(x1)) -> c_9(q0^#(x1))}
{y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))}
==> {q2^#(x(x1)) -> c_9(q0^#(x1))}
{y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))}
==> {q2^#(x(x1)) -> c_9(q0^#(x1))}
{q2^#(x(x1)) -> c_9(q0^#(x1))}
==> {q0^#(y(x1)) -> c_10(y^#(q3(x1)))}
{q2^#(x(x1)) -> c_9(q0^#(x1))}
==> {q0^#(a(x1)) -> c_0(q1^#(x1))}
{q0^#(y(x1)) -> c_10(y^#(q3(x1)))}
==> {y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))}
{q0^#(y(x1)) -> c_10(y^#(q3(x1)))}
==> {y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))}
{q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
==> {y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))}
{q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
==> {y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))}
We consider the following path(s):
1) { q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))}
The usable rules for this path are the following:
{ q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [0]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [0]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
q1^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [8]
a^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [0]
y^#(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [1]
q2^#(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [1] x1 + [0]
q3^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))}
and weakly orienting the rules
{ q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [1]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [0]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
q1^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [8]
c_2(x1) = [1] x1 + [0]
y^#(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [15]
q2^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [1] x1 + [3]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [1] x1 + [0]
q3^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))}
and weakly orienting the rules
{ a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [1]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [1]
q4(x1) = [1] x1 + [1]
q0^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
q1^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [0]
y^#(x1) = [1] x1 + [4]
c_3(x1) = [1] x1 + [0]
q2^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [1] x1 + [0]
q3^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{q0^#(a(x1)) -> c_0(q1^#(x1))}
and weakly orienting the rules
{ y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{q0^#(a(x1)) -> c_0(q1^#(x1))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [1]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [13]
bl(x1) = [1] x1 + [4]
q4(x1) = [1] x1 + [5]
q0^#(x1) = [1] x1 + [3]
c_0(x1) = [1] x1 + [0]
q1^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [8]
a^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [8]
y^#(x1) = [1] x1 + [15]
c_3(x1) = [1] x1 + [0]
q2^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [15]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [1] x1 + [2]
c_10(x1) = [1] x1 + [0]
q3^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [1]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
and weakly orienting the rules
{ q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [1]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [0]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
q1^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [1]
y^#(x1) = [1] x1 + [5]
c_3(x1) = [1] x1 + [0]
q2^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [1] x1 + [1]
q3^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [1]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))}
and weakly orienting the rules
{ q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [1]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [3]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [14]
bl(x1) = [1] x1 + [2]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [2]
c_0(x1) = [1] x1 + [1]
q1^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [1]
y^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [0]
q2^#(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [1] x1 + [2]
q3^#(x1) = [1] x1 + [15]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))}
and weakly orienting the rules
{ q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [1]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [8]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [15]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [4]
c_0(x1) = [1] x1 + [0]
q1^#(x1) = [1] x1 + [4]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [0]
y^#(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [0]
q2^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [1] x1 + [0]
q3^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ a(q1(b(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))}
and weakly orienting the rules
{ q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ a(q1(b(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [0]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [2]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [10]
q2(x1) = [1] x1 + [4]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [2]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
q1^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [0]
y^#(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [1]
q2^#(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [9]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [1] x1 + [0]
q3^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [2]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{q0(a(x1)) -> x(q1(x1))}
and weakly orienting the rules
{ a(q1(b(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{q0(a(x1)) -> x(q1(x1))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [0]
a(x1) = [1] x1 + [2]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [0]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [0]
q3(x1) = [1] x1 + [0]
bl(x1) = [1] x1 + [1]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
q1^#(x1) = [1] x1 + [1]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [3]
c_2(x1) = [1] x1 + [0]
y^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [0]
q2^#(x1) = [1] x1 + [1]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [1] x1 + [0]
q3^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [7]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{q0(y(x1)) -> y(q3(x1))}
and weakly orienting the rules
{ q0(a(x1)) -> x(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{q0(y(x1)) -> y(q3(x1))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [4]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [1]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [7]
q2(x1) = [1] x1 + [8]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [0]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [1] x1 + [4]
c_0(x1) = [1] x1 + [0]
q1^#(x1) = [1] x1 + [4]
c_1(x1) = [1] x1 + [0]
a^#(x1) = [1] x1 + [2]
c_2(x1) = [1] x1 + [1]
y^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [0]
q2^#(x1) = [1] x1 + [9]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [1] x1 + [5]
c_10(x1) = [1] x1 + [1]
q3^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [1]
c_12() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q3(y(x1)) -> y(q3(x1))}
Weak Rules:
{ q0(y(x1)) -> y(q3(x1))
, q0(a(x1)) -> x(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, q3(y(x1)) -> y(q3(x1))}
Weak Rules:
{ q0(y(x1)) -> y(q3(x1))
, q0(a(x1)) -> x(q1(x1))
, a(q1(b(x1))) -> q2(a(y(x1)))
, y(q1(b(x1))) -> q2(y(y(x1)))
, q0^#(y(x1)) -> c_10(y^#(q3(x1)))
, q1^#(y(x1)) -> c_2(y^#(q1(x1)))
, q1^#(a(x1)) -> c_1(a^#(q1(x1)))
, q2^#(x(x1)) -> c_9(q0^#(x1))
, a^#(q1(b(x1))) -> c_3(q2^#(a(y(x1))))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q0^#(a(x1)) -> c_0(q1^#(x1))
, y^#(q2(y(x1))) -> c_8(q2^#(y(y(x1))))
, y^#(q2(a(x1))) -> c_7(q2^#(y(a(x1))))
, y^#(q1(b(x1))) -> c_6(q2^#(y(y(x1))))
, a^#(q2(y(x1))) -> c_5(q2^#(a(y(x1))))
, a^#(q2(a(x1))) -> c_4(q2^#(a(a(x1))))
, q3(bl(x1)) -> bl(q4(x1))
, q2(x(x1)) -> x(q0(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ x_0(3) -> 3
, x_0(6) -> 3
, x_0(9) -> 3
, x_0(10) -> 3
, b_0(3) -> 6
, b_0(6) -> 6
, b_0(9) -> 6
, b_0(10) -> 6
, bl_0(3) -> 9
, bl_0(6) -> 9
, bl_0(9) -> 9
, bl_0(10) -> 9
, q4_0(3) -> 10
, q4_0(6) -> 10
, q4_0(9) -> 10
, q4_0(10) -> 10
, q0^#_0(3) -> 11
, q0^#_0(6) -> 11
, q0^#_0(9) -> 11
, q0^#_0(10) -> 11
, q1^#_0(3) -> 13
, q1^#_0(6) -> 13
, q1^#_0(9) -> 13
, q1^#_0(10) -> 13
, a^#_0(3) -> 15
, a^#_0(6) -> 15
, a^#_0(9) -> 15
, a^#_0(10) -> 15
, y^#_0(3) -> 17
, y^#_0(6) -> 17
, y^#_0(9) -> 17
, y^#_0(10) -> 17
, q2^#_0(3) -> 19
, q2^#_0(6) -> 19
, q2^#_0(9) -> 19
, q2^#_0(10) -> 19
, c_9_0(11) -> 19
, q3^#_0(3) -> 27
, q3^#_0(6) -> 27
, q3^#_0(9) -> 27
, q3^#_0(10) -> 27}
2) {q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
The usable rules for this path are the following:
{ q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, q2(x(x1)) -> x(q0(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ q3(y(x1)) -> y(q3(x1))
, q3(bl(x1)) -> bl(q4(x1))
, y(q1(b(x1))) -> q2(y(y(x1)))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, a(q1(b(x1))) -> q2(a(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, q2(x(x1)) -> x(q0(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ q3(bl(x1)) -> bl(q4(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ q3(bl(x1)) -> bl(q4(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [4]
a(x1) = [1] x1 + [4]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [0]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [0]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
q1^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
y^#(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
q2^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
q3^#(x1) = [1] x1 + [1]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
and weakly orienting the rules
{ q3(bl(x1)) -> bl(q4(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{q3^#(y(x1)) -> c_11(y^#(q3(x1)))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [1]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [0]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [1]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [7]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
q1^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
y^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
q2^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
q3^#(x1) = [1] x1 + [5]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ y(q1(b(x1))) -> q2(y(y(x1)))
, a(q1(b(x1))) -> q2(a(y(x1)))}
and weakly orienting the rules
{ q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q3(bl(x1)) -> bl(q4(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ y(q1(b(x1))) -> q2(y(y(x1)))
, a(q1(b(x1))) -> q2(a(y(x1)))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [8]
a(x1) = [1] x1 + [2]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [8]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
q2(x1) = [1] x1 + [0]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [15]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
q1^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
y^#(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
q2^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
q3^#(x1) = [1] x1 + [9]
c_11(x1) = [1] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{q2(x(x1)) -> x(q0(x1))}
and weakly orienting the rules
{ y(q1(b(x1))) -> q2(y(y(x1)))
, a(q1(b(x1))) -> q2(a(y(x1)))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q3(bl(x1)) -> bl(q4(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{q2(x(x1)) -> x(q0(x1))}
Details:
Interpretation Functions:
q0(x1) = [1] x1 + [4]
a(x1) = [1] x1 + [0]
x(x1) = [1] x1 + [0]
q1(x1) = [1] x1 + [0]
y(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [12]
q2(x1) = [1] x1 + [8]
q3(x1) = [1] x1 + [1]
bl(x1) = [1] x1 + [15]
q4(x1) = [1] x1 + [0]
q0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
q1^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
y^#(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
q2^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
q3^#(x1) = [1] x1 + [11]
c_11(x1) = [1] x1 + [7]
c_12() = [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ q3(y(x1)) -> y(q3(x1))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))}
Weak Rules:
{ q2(x(x1)) -> x(q0(x1))
, y(q1(b(x1))) -> q2(y(y(x1)))
, a(q1(b(x1))) -> q2(a(y(x1)))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q3(bl(x1)) -> bl(q4(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ q3(y(x1)) -> y(q3(x1))
, y(q2(a(x1))) -> q2(y(a(x1)))
, y(q2(y(x1))) -> q2(y(y(x1)))
, a(q2(a(x1))) -> q2(a(a(x1)))
, a(q2(y(x1))) -> q2(a(y(x1)))
, q1(a(x1)) -> a(q1(x1))
, q1(y(x1)) -> y(q1(x1))}
Weak Rules:
{ q2(x(x1)) -> x(q0(x1))
, y(q1(b(x1))) -> q2(y(y(x1)))
, a(q1(b(x1))) -> q2(a(y(x1)))
, q3^#(y(x1)) -> c_11(y^#(q3(x1)))
, q3(bl(x1)) -> bl(q4(x1))
, q0(a(x1)) -> x(q1(x1))
, q0(y(x1)) -> y(q3(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ x_0(3) -> 3
, x_0(6) -> 3
, x_0(9) -> 3
, x_0(10) -> 3
, b_0(3) -> 6
, b_0(6) -> 6
, b_0(9) -> 6
, b_0(10) -> 6
, bl_0(3) -> 9
, bl_0(6) -> 9
, bl_0(9) -> 9
, bl_0(10) -> 9
, q4_0(3) -> 10
, q4_0(6) -> 10
, q4_0(9) -> 10
, q4_0(10) -> 10
, y^#_0(3) -> 17
, y^#_0(6) -> 17
, y^#_0(9) -> 17
, y^#_0(10) -> 17
, q3^#_0(3) -> 27
, q3^#_0(6) -> 27
, q3^#_0(9) -> 27
, q3^#_0(10) -> 27}
3) {q3^#(bl(x1)) -> c_12()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
q0(x1) = [0] x1 + [0]
a(x1) = [0] x1 + [0]
x(x1) = [0] x1 + [0]
q1(x1) = [0] x1 + [0]
y(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
q2(x1) = [0] x1 + [0]
q3(x1) = [0] x1 + [0]
bl(x1) = [0] x1 + [0]
q4(x1) = [0] x1 + [0]
q0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
q1^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
y^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
q2^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
q3^#(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {q3^#(bl(x1)) -> c_12()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{q3^#(bl(x1)) -> c_12()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{q3^#(bl(x1)) -> c_12()}
Details:
Interpretation Functions:
q0(x1) = [0] x1 + [0]
a(x1) = [0] x1 + [0]
x(x1) = [0] x1 + [0]
q1(x1) = [0] x1 + [0]
y(x1) = [0] x1 + [0]
b(x1) = [0] x1 + [0]
q2(x1) = [0] x1 + [0]
q3(x1) = [0] x1 + [0]
bl(x1) = [1] x1 + [0]
q4(x1) = [0] x1 + [0]
q0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
q1^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
a^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
y^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
q2^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
q3^#(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12() = [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {q3^#(bl(x1)) -> c_12()}
Details:
The given problem does not contain any strict rules